#ifndef CTLLEXER_HH_
# define CTLLEXER_HH_

///
/// \file CTLLexer.hh
/// \brief Definition of the lexer.
/// \author Coddy Levi, Sylvain Lobry
/// \version 1.0
///
/// Definition of the class implementing the formula lexer.
///

# include <string>
# include <vector>


///
/// \struct symbols
/// \brief The symbols used by the lexer.
///
/// The symbols that identify the elements we can find in a formula.
/// These are the output of the lexer.
///
typedef enum
  {
    AND, ///< Operator And.
    OR, ///< Operator Or.
    NOT, ///< Operator Not.
    IMPLIES, ///< Operator Implies.
    AX, ///< Operator AX.
    EX, ///< Operator EX.
    AF, ///< Operator AF.
    EF, ///< Operator EF.
    AG, ///< Operator AG.
    EG, ///< Operator EG.
    AU, ///< Operator AU.
    EU, ///< Operator EU.
    T, ///< Value true.
    F, ///< Value false.

    LPAR, ///< Left parenthesis.
    RPAR, ///< Right parenthesis.
    COMMA, ///< Comma separating arguments.

    VAR ///< A variable..
  } symbols;



///
/// \class CTLLexer
/// \brief The class that implements the lexer.
///
class CTLLexer
{
private:
  ///
  /// The input formula.
  ///
  std::string		formula_;

  ///
  /// An unsigned representing the current position of the lexer into the formula.
  ///
  unsigned		offset_;

  ///
  /// A vector storing the variables in the formula (stored in the same order as
  /// their apparition).
  ///
  std::vector<std::string> vars_;

  ///
  /// Our position in the vars_ vector (used in getNextVar ()).
  ///
  unsigned		offset_var_;

  bool
  isNextToken (std::string test);

  void
  pushNextVar ();

public:
  ///
  /// \brief Main constructor of the lexer.
  ///
  /// \param[in]	formula The formula to be tokenized
  ///
  CTLLexer (std::string	formula);

  ///
  /// \brief return the next token of the formula.
  ///
  /// \return		The next token.
  ///
  symbols
  getNextToken ();

  ///
  /// \brief return the next variable stored in the vector.
  ///
  /// \return		The next variable.
  ///
  std::string
  getNextVar ();

  ///
  /// \brief Indicates if we have reached the end of the formula.
  ///
  /// \return		true if we have reached the end of the document.
  ///			false otherwise.
  ///
  bool
  eof ();

  ///
  /// \brief Return the current position of the lexer in the formula.
  ///
  /// \return		The position in the formula.
  ///
  unsigned
  getOffset ();
};

#endif /* !CTLLEXER_HH_ */
